R-consistent(R; es)
== es_realizer_ind(R;
== es_realizer_ind(True;
== es_realizer_ind(left,right,rec1,rec2.(rec1  rec2);
== es_realizer_ind(i,T,x,V.case V
== es_realizer_ind(of inl(v) => init-p(es; i; T; x; v)
== es_realizer_ind(o| inr(v) => init_p(es; i; T; x; v);
== es_realizer_ind(i,T,x,L.frame-p(es; i; T; x; L);
== es_realizer_ind(l,tg,L.sframe-p(es; l; tg; L);
== es_realizer_ind(i,ds,k,T,x,F.case F
== es_realizer_ind(of inl(f) => effect-p(es; i; ds; k; T; x; f)
== es_realizer_ind(o| inr(f) => effect_p(es; i; ds; k; T; x; f);
== es_realizer_ind(ds,k,T,l,dt,g.sends-p(es; ds; k; T; l; dt; g);
== es_realizer_ind(i,ds,a,prob,P.pre-p(es; i; ds; a; prob; P);
== es_realizer_ind(i,k,L.aframe-p(es; i; k; L);
== es_realizer_ind(i,k,L.bframe-p(es; i; k; L);
== es_realizer_ind(i,x,L.rframe-p(es; i; x; L)) 

latex

Definitions	es realizer ind, True, P  Q, init-p(es; i; T; x; v), init_p(es; i; T; x; v), frame-p(es; i; T; x; L), sframe-p(es; l; tg; L), case b of inl(x) => s(x) | inr(y) => t(y), effect-p(es; i; ds; k; T; x; f), effect_p(es; i; ds; k; T; x; f), sends-p(es; ds; k; T; l; dt; g), pre-p(es; i; ds; a; p; P), aframe-p(es; i; k; L), bframe-p(es; i; k; L), rframe-p(es; i; x; L)
FDL editor aliases	R-consistent